(set-logic QF_LRA)
(set-info :source | Clock Synchronization. Bruno Dutertre (bruno@csl.sri.com) |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)

(set-option :split-type lookahead)
(set-option :split-num 20)
(set-option :split-asap true)
(set-option :split-format smt2)
(set-option :split-format-length "brief")
(set-option :output-dir "splits_here")
(set-option :sat_split_test_cube_and_conquer true)

(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(assert (let
 ((?v_0 (+ x_0 (/ 999 1000)))
 (?v_1 (+ x_0 (/ 1001 1000)))
 (?v_2 (not (<= (- 1 1) (+ (+ (+ x_6 x_7) (* (* (+ x_8 x_5) 2) (/ 1 999))) (/ 2335 666)))))) (and (and (and (and (and (and (and (and (and (and (and (and (and (not (<= x_4 0)) (not (<= x_5 0))) (not (<= x_6 0))) (not (< x_7 (+ x_6 (* (* (+ (* (* x_5 1) (/ 1 2)) 1) 1001) (/ 1 999)))))) (< x_8 (- (* (* (- (- x_5 x_7) 1) 999) (/ 1 2)) 1))) (not (< x_8 (* (* (+ (+ (+ x_4 x_6) x_7) (/ 1501 1000)) 1001) (/ 1 999))))) (= x_0 0)) (<= ?v_0 x_1)) (<= x_1 ?v_1)) (<= ?v_0 x_2)) (<= x_2 ?v_1)) (<= ?v_0 x_3)) (<= x_3 ?v_1)) (or (or (or (or (or (or (or (or ?v_2 ?v_2) ?v_2) ?v_2) ?v_2) ?v_2) ?v_2) ?v_2) ?v_2))))
(check-sat)
(exit)
